1. Field of the Invention
The present invention relates to a technology for supporting hardware logic verification.
2. Description of the Related Art
Conventionally, a hardware module is generally configured to operate normally when an input pattern provided in a specification is received. If an input pattern that is not originally permitted is received, no operation is specified. Therefore, when a logic simulation is performed for each module, the input pattern to be input into the module should be one provided in the specification. Otherwise, a significant simulation result cannot be obtained.
The input pattern can be created using a pattern manually created in advance. The input pattern can also be created using a pattern generator that dynamically and automatically generates a pattern while performing a simulation. Furthermore, the input pattern can be created using a combination of the manually-created pattern and the pattern generator.
Ordinarily, the pattern generator is manually created using a language, such as C programming language, SystemC language, Verilog language, and very high speed integrated circuit (VHSIC) hardware description language (VDHL). Moreover, in recent years, a technology that automatically generates the pattern generator from a description related to a formal input-restriction condition has also become known (for example, in Proc. of the Design Automation Conference 2003, pp. 296 and 299, 2003, titled “Constraint Synthesis for Environment Modeling in Functional Verification” by J. Yuan, Ken Albin, Adnan Aziz, and Carl Pixley). The input-restriction condition is a condition that must be always satisfied by an input sent to a hardware module to be verified.
FIG. 14 is a schematic of a hardware module to be verified. A verification subject 1400 is a sequential circuit. clk is a clock input. The verification subject 1400 has 1-bit inputs cmd and req, a 1-bit output ack, a 32-bit input wd, and a 32-bit output rd. Following input-restriction conditions apply to the inputs of the verification subject.
When cmd=0 and req=1 are input, a Read operation starts. Values of cmd and req cannot be changed until the Read operation is completed by a response of ack=1.
When cmd=1 and req=1 are input, a Write operation starts. Values of cmd, req, and wd cannot be changed until the Write operation is completed by a response of ack=1.
As in the example above, the input-restriction conditions are generally dependent on not only input and output values that are input into and output from the verification subject 1400 at the current time, but also past input and output values. Therefore, a set-up that judges whether an input restriction is followed is introduced.
FIG. 15 is a schematic of a model defining the input-restriction condition. In the example shown in FIG. 15, a modeling of the set-up used to judge whether the input restriction is followed is performed using a sequential machine M0 and a logical expression C0. The logical expression C0 corresponds to the input-restriction condition. The sequential machine M0 has a state variable s and a state variable t. The state variable s and the state variable t indicate an operation state of the verification subject 1400 (sequential circuit) and input and output values.
FIG. 16 is a schematic of a state transition graph expressing value changes of the state variable s. s=0 corresponds to an initial state. s=1 corresponds to a state during the Read operation. s=2 corresponds to a state during the Write operation. The state variable t always maintains a wd value of a cycle immediately prior to the present cycle. The input-restriction condition is expressed by the logical expression C0 shown in a following Equation 1, using the state variable s and the state variable t of the sequential machine M0, and the input and output values of the verification subject.C0=(s=0)+(s=1)· cmd·req+(s=2)·cmd·req·(wd=t)  (1)
A pattern generator (G0) can be automatically generated with the logical expression C0 of the input-restriction condition as a starting point. FIG. 17 is a schematic of a pattern generator (G0) automatically generated with the logical expression C0 of the input-restriction condition as the starting point. The pattern generator (G0) shown in FIG. 17 performs operations shown in following logical expressions 2 to 4.cmd←(s=1)?0:(s=2)?1:random(1)  (2)req←((s=1)+(s=2))?1:random(1)  (3)wd←(s=2)?t:random(32)  (4)
A logical expression “x?y:z” is a ternary operation having a value y when a condition x is met and a value z when the condition x is not met, and is equivalent to a following logical expression 5. “random(n)” is a function that generates a random value having a bit width of n. For example, in the logical expression 4, wd has a value t when the verification subject is performing the Write operation. wd has a random value of 32 bits when the verification subject is not performing the Write operation.x?y:z  (5)
An input group input into the verification subject include <y>=(y1, y2, . . . , yn) of n bits. A group of other variables (the outputs output from the verification subject and the state variables of the sequential machine added to the verification subject) includes <x>=(x1, x2, . . . , xm) of m bits. <x> and <y> are respectively vectors formed using the variables within the parentheses.
The logical expression provided as an input restriction is equivalent to a logical function f of <x> and <y>. Therefore, a target pattern generator (G0) can be configured as follows:
                              y          1                ⟵                              g            1                    ⁡                      (                                          x                →                            ,                              r                1                                      )                                                            y          2                ⟵                              g            2                    ⁡                      (                                          x                →                            ,                              r                1                            ,                              r                2                                      )                                          ⋮                                    y          n                ⟵                              g            n                    ⁡                      (                                          x                →                            ,                              r                1                            ,                              r                2                            ,              …              ⁢                                                          ,                              r                n                                      )                              
r1, r2, . . . , rn are newly introduced logical variables randomly having a value of 1 or 0. A logical function group g1, g2, . . . , gn is determined by following procedures [1] to [5].
[1] Under an assumption that y2, . . . , yn are set to appropriate values of some sort, a simplified restriction condition is determined. The restriction condition is expressed by Equation 6.f′({right arrow over (x)},y1)=∃(y2, . . . ,yn)·f({right arrow over (x)},{right arrow over (y)})  (6)
[2] A condition in which a value 0 can be output to y1 and a condition in which a value 1 can be output to y1 are determined by an assignment of a constant to Equation 6. Using the conditions, a logical function g1 in Equation 7 below, is configured to have the value 0 when 0 can be output but 1 cannot be output to y1, the value 1 when 1 can be output but 0 cannot be output to y1, and a value equivalent to the random value r1 in other instances.g1({right arrow over (x)},r1)=f′({right arrow over (x)}, 0)· f′({right arrow over (x)}, 1)?0: f′({right arrow over (x)},0)·f′({right arrow over (x)},1)?1:r1  (7)
[3] The value of the logical function g1 in Equation 7 is used as y1. Under an assumption that y3, . . . , yn are set to appropriate values of some sort, a simplified restriction condition is determined. The restriction condition is expressed by Equation 8.f″({right arrow over (x)},r1,y2)=∃(y3, . . . ,yn)·f({right arrow over (x)}, g1({right arrow over (x)},r1),y2,y3, . . . ,yn)  (8)
[4] A new logical function g2 is determined using a same procedure as in [2]. The logical function g2 is expressed by Equation 9.g2({right arrow over (x)},r1,r2)=f″({right arrow over (x)},r1,0)· f({right arrow over (x)},r1, 1)?0: f″({right arrow over (x)},r1,0)·f″({right arrow over (x)},r1,1)?1:r2  (9)
[5] Subsequent logical functions up to a logical function gn are determined using the same procedure. A ∃v.f operation accurately determines “a condition related to remaining variables to allow an existence of an assignment of a value to v in which a value of the logical function f is 1”. When a variable vi is a one-bit logical variable, an ∃ operation is defined as follows:
                              ∃                                    v              i                        ·                          f              ⁡                              (                                                      v                    1                                    ,                  …                  ⁢                                                                          ,                                      v                    i                                    ,                  …                  ⁢                                                                          ,                                      v                    n                                                  )                                                    =                              f            ⁡                          (                                                v                  1                                ,                …                ⁢                                                                  ,                0                ,                …                ⁢                                                                  ,                                  v                  n                                            )                                +                      f            ⁡                          (                                                v                  1                                ,                …                ⁢                                                                  ,                1                ,                …                ⁢                                                                  ,                                  v                  n                                            )                                                          (        10        )            
When the variable vi is a multiple value variable having a set of values V, an ∃ operation is defined as follows:
                              ∃                                    v              i                        ·                          f              ⁡                              (                                                      v                    1                                    ,                  …                  ⁢                                                                          ,                                      v                    i                                    ,                  …                  ⁢                                                                          ,                                      x                    v                                                  )                                                    =                              ∑                          a              ∈              V                                                                      ⁢                      f            ⁡                          (                                                v                  1                                ,                …                ⁢                                                                  ,                a                ,                …                ⁢                                                                  ,                                  v                  n                                            )                                                          (        11        )            
An ∃ operation related to a variable group (y1, . . . , ym) is defined as follows:∃ y.f=∃y1 . . . ∃y m.f  (12)
It is widely known that the ∃ operation can be effectively executed by a calculator using a technology, such as a binary decision diagram (BDD). When a logical expression including a multiple-bit input variable, such as wd in Equation 1, is the starting point, the logical expression is used after being rewritten into, for example, Equation 13. Equation 13 is divided into each bit.
                              C          0                =                              (                          s              =              0                        )                    +                                    (                              s                =                1                            )                        ·                          cmd              _                        ·            req                    +                                                    (                                  s                  +                  2                                )                            ·              cmd              ·              req              ·                              (                                                      wd                    ⁡                                          [                      31                      ]                                                        =                                      t                    ⁡                                          [                      31                      ]                                                                      )                                      ⁢                          …              ⁡                              (                                                      wd                    ⁡                                          [                      0                      ]                                                        =                                      t                    ⁡                                          [                      0                      ]                                                                      )                                                                        (        13        )            
Alternatively, as a different method, a one-bit variable wd_t can be introduced and the logical expression can be rewritten as follows. The one-bit variable wd_t indicates that a wd=t relationship is established.C0=(s=0)+(s=1)· cmd·req+(s=2)·cmd·req·wd—t  (14)
Examples in which the logical functions g1, g2, and g3 are determined with Equation 6 as the starting point are shown in [1] to [6] below. The logical functions g1, g2, and g3 are equivalent to the right-hand sides of Equations 2 to 4 above.
[1] Under an assumption that req and wd_t are set to appropriate values of some sort, a simplified restriction condition f′(s, cmd) is determined. The restriction condition f′(s, cmd) is expressed by Equation 15.
                                                                                          f                  ′                                ⁡                                  (                                      s                    ,                    cmd                                    )                                            =                            ⁢                              ∃                                                      (                                          req                      ,                      wd_t                                        )                                    ·                                      (                                                                  (                                                  s                          =                          0                                                )                                            +                                                                        (                                                      s                            =                            1                                                    )                                                ·                                                  cmd                          _                                                ·                        req                                            +                                                                                                                                                            ⁢                                                (                                      s                    =                    2                                    )                                ·                cmd                ·                req                ·                wd_t                            )                                                                          =                            ⁢                                                (                                      s                    =                    0                                    )                                +                                                      (                                          s                      =                      1                                        )                                    ·                                      cmd                    _                                                  +                                                      (                                          s                      =                      2                                        )                                    ·                  cmd                                                                                        (        15        )            
[2] A condition f′(s, 0) in which a value 0 can be output to cmd and a condition f′(s, 1) in which a value 1 can be output to cmd are determined by an assignment of a constant to the restriction condition f′(s, cmd). Using the conditions, a logical function g1 (s, r1) is configured to have the value 0 when 0 can be output but 1 cannot be output to cmd, the value 1 when 1 can be output but 0 cannot be output to cmd, and a value equivalent to the random value r1 in other instances. The condition f′(s, 0), the condition f′(s, 1), and the logical function g1(s, r1) are expressed by Equations 16 to 18.
                                          f            ′                    ⁡                      (                          s              ,              0                        )                          =                              (                          s              =              0                        )                    +                      (                          s              =              1                        )                                              (        16        )                                                      f            ′                    ⁡                      (                          s              ,              1                        )                          =                              (                          s              =              0                        )                    +                      (                          s              =              2                        )                                              (        17        )                                                                                                      g                  1                                ⁡                                  (                                      s                    ,                                          r                      1                                                        )                                            =                            ⁢                                                                                          f                      ′                                        ⁡                                          (                                              s                        ,                        0                                            )                                                        ·                                                                                                              f                          ′                                                ⁡                                                  (                                                      s                            ,                            1                                                    )                                                                    _                                        ?                    0                                                  ⁢                                  :                                ⁢                                                                                                    f                        ′                                            ⁡                                              (                                                  s                          ,                          0                                                )                                                              _                                    ·                                                                                    f                        ′                                            ⁡                                              (                                                  s                          ,                          1                                                )                                                              ?                    1                                                  ⁢                                  :                                ⁢                                  r                  1                                                                                                        =                            ⁢                                                                    (                                          s                      =                      1                                        )                                    ?                  0                                ⁢                                  :                                ⁢                                                      (                                          s                      =                      2                                        )                                    ?                  1                                ⁢                                  :                                ⁢                                  r                  1                                                                                        (        18        )            
[3] The value of the logical function g1(s, r1) is used as cmd. Under an assumption that wd_t is set to an appropriate value of some sort, a simplified restriction condition f″(s, r1, req) is determined. The restriction condition f″(s, r1, req) is expressed by Equation 19.
                                                                                          f                  ″                                ⁡                                  (                                      s                    ,                                          r                      1                                        ,                    req                                    )                                            =                            ⁢                              ∃                                                      (                    wd_t                    )                                    ·                                      (                                                                  (                                                  s                          =                          0                                                )                                            +                                                                        (                                                      s                            =                            1                                                    )                                                ·                                                                                                            g                              1                                                        ⁡                                                          (                                                              s                                ,                                                                  r                                  1                                                                                            )                                                                                _                                                ·                        req                                            +                                                                                                                                                            ⁢                                                (                                      s                    =                    2                                    )                                ·                                                      g                    1                                    ⁡                                      (                                          s                      ,                                              r                        1                                                              )                                                  ·                req                ·                wd_t                            )                                                                          =                            ⁢                              ∃                                                      (                    wd_t                    )                                    ·                                      (                                                                  (                                                  s                          =                          0                                                )                                            +                                                                        (                                                      s                            =                            1                                                    )                                                ·                        req                                            +                                                                                                                                                            ⁢                                                (                                      s                    =                    2                                    )                                ·                req                ·                wd_t                            )                                                                          =                            ⁢                                                (                                      s                    =                    0                                    )                                +                                                      (                                          s                      =                      1                                        )                                    ·                  req                                +                                                      (                                          s                      =                      2                                        )                                    ·                  req                                                                                        (        19        )            
[4] A condition f″(s, r1, 0) in which a value 0 can be output to req and a condition f″(s, r1, 1) in which a value 1 can be output to req are determined by an assignment of a constant to the restriction condition f″(s, r1, req). Using the conditions, a logical function g2 (s, r1, r2) is configured to have the value 0 when 0 can be output but 1 cannot be output to req, the value 1 when 1 can be output but 0 cannot be output to req, and a value equivalent to a random value r2in other instances. The condition f″(s, r1, 0), the condition f″(s, r1, 1), and the logical function g2 (s, r1, r2) are expressed by Equations 20 to 22.
                                          f            ″                    ⁡                      (                          s              ,                              r                1                            ,              0                        )                          =                  (                      s            =            0                    )                                    (        20        )                                                      f            ″                    ⁡                      (                          s              ,                              r                1                            ,              1                        )                          =                              (                          s              =              0                        )                    +                      (                          s              =              1                        )                    +                      (                          s              =              2                        )                                              (        21        )                                                                                                      g                  2                                ⁡                                  (                                      s                    ,                                          r                      1                                        ,                                          r                      2                                                        )                                            =                            ⁢                                                                                          f                      ″                                        ⁡                                          (                                              s                        ,                                                  r                          1                                                ,                        0                                            )                                                        ·                                                                                                              f                          ″                                                ⁡                                                  (                                                      s                            ,                                                          r                              1                                                        ,                            1                                                    )                                                                    _                                        ?                    0                                                  ⁢                                  :                                ⁢                                                                                                    f                        ″                                            ⁡                                              (                                                  s                          ,                                                      r                            1                                                    ,                          0                                                )                                                              _                                    ·                                                                                                                      ⁢                                                                                          f                      ″                                        ⁡                                          (                                              s                        ,                                                  r                          1                                                ,                        1                                            )                                                        ?                  1                                :                                  r                  2                                                                                                        =                            ⁢                                                0                  ?                  0                                ⁢                                  :                                ⁢                                                      (                                                                  (                                                  s                          =                          1                                                )                                            +                                              (                                                  s                          =                          2                                                )                                                              )                                    ?                  1                                ⁢                                  :                                ⁢                                  r                  2                                                                                                        =                            ⁢                                                                    (                                                                  (                                                  s                          =                          1                                                )                                            +                                              (                                                  s                          =                          2                                                )                                                              )                                    ?                  1                                ⁢                                  :                                ⁢                                  r                  2                                                                                        (        22        )            
[5] A restriction condition f′″(s, r1, r2, wd_t) of when the value of the logical function g1(s, r1) is used as cmd and the value of the logical function g2(s, r1, r2) is used as req is determined. The t) is expressed by Equation 23.□ restriction condition f′″(s, r1, r2, wd
                                                                                          f                  ′′′                                ⁡                                  (                                      s                    ,                                          r                      1                                        ,                                          r                      2                                        ,                    wd_t                                    )                                            =                            ⁢                                                (                                      s                    =                    0                                    )                                +                                                      (                                          s                      =                      1                                        )                                    ·                                                                                    g                        1                                            ⁡                                              (                                                  s                          ,                                                      r                            1                                                                          )                                                              _                                    ·                                                                                                                      ⁢                                                                    g                    2                                    ⁡                                      (                                          s                      ,                                              r                        1                                            ,                                              r                        2                                                              )                                                  +                                                      (                                          s                      =                      2                                        )                                    ·                                                            g                      1                                        ⁡                                          (                                              s                        ,                                                  r                          1                                                                    )                                                        ·                                                                                                                      ⁢                                                                    g                    2                                    ⁡                                      (                                          s                      ,                                              r                        1                                            ,                                              r                        2                                                              )                                                  ·                wd_t                                                                                        =                            ⁢                                                (                                      s                    =                    0                                    )                                +                                  (                                      s                    =                    1                                    )                                +                                                      (                                          s                      =                      2                                        )                                    ·                  wd_t                                                                                        (        23        )            
[6] A condition f′″(s, r1, r2, 0) in which a value 0 can be output to wd_t and a condition f′″(s, r1, r2, 1) in which a value 1 can be output to wd_t are determined by an assignment of a constant to the restriction condition f′″(s, r1, r2, wd_t). Using the conditions, a logical function g3(s, r1, r2, r3) is configured to have the value 0 when 0 can be output but 1 cannot be output to wd_t, the value 1 when 1 can be output but 0 cannot be output to wd_t, and a value equivalent to a random value r3 in other instances. The condition f′″(s, r1, r2, 0), the condition f′″(s, r1, r2, 1), and the logical function g3(s, r1, r2, r3) are expressed by Equations 24 to 26.
                                          f            ′′′                    ⁡                      (                          s              ,                              r                1                            ,                              r                2                            ,              0                        )                          =                              (                          s              =              0                        )                    +                      (                          s              =              1                        )                                              (        24        )                                                      f            ′′′                    ⁡                      (                          s              ,                              r                1                            ,                                                r                  2                                ⁢                1                                      )                          =                              (                          s              =              0                        )                    +                      (                          s              =              1                        )                    +                      (                          s              =              2                        )                                              (        25        )                                                                                                      g                  3                                ⁡                                  (                                      s                    ,                                          r                      1                                        ,                                          r                      2                                        ,                                          r                      3                                                        )                                            =                            ⁢                                                                                          f                      ′′′                                        ⁡                                          (                                              s                        ,                                                  r                          1                                                ,                                                  r                          2                                                ,                        0                                            )                                                        ·                                                                                    f                        ′′′                                            ⁡                                              (                                                  s                          ,                                                      r                            1                                                    ,                                                      r                            2                                                    ,                          1                                                )                                                              ?                    0                                                  ⁢                                  :                                                                                                                       ⁢                                                                                                                  f                        ′′′                                            ⁡                                              (                                                  s                          ,                                                      r                            1                                                    ,                                                      r                            2                                                    ,                          0                                                )                                                              _                                    ·                                                                                    f                        ′′′                                            ⁡                                              (                                                  s                          ,                                                      r                            1                                                    ,                                                      r                            2                                                    ,                          1                                                )                                                              ?                    1                                                  ⁢                                  :                                ⁢                                  r                  3                                                                                                        =                            ⁢                                                0                  ?                  0                                ⁢                                  :                                ⁢                                                      (                                          s                      =                      2                                        )                                    ?                  1                                ⁢                                  :                                ⁢                                  r                  3                                                                                                        =                            ⁢                                                                    (                                          s                      =                      2                                        )                                    ?                  1                                :                                  r                  3                                                                                        (        26        )            
The values of g1 and g2 are respectively assigned to cmd and req. cmd and req are one-bit variables. The values of the variables r1 and r2 are newly generated each time, using a random value generating function, random(1).
A 32-bit random value, excluding t, is assigned to the 32-bit variable wd based on g3, when wd_t, namely the value of g3, is 0. The value of t is assigned to the 32-bit variable wd as is when the value of g3 is 1. An arbitrary 32-bit random value is assigned to the 32-bit variable wd when the value of g3 is a random value. As a result, a logical expression G0 (Equations 27 to 29 below) expressing an operation of the pattern generator (G0) can be obtained.cmd←(s=1)?0:(s=2)?1:random(1)  (27)req←((s=1)+(s=2))?1:random(1)  (28)wd—t←(s=2)?t:random(32)  (29)
A creator of a logic verification environment is required to create or automatically generate an input pattern, taking into consideration a balance between following two different types of requests:    (i) targeting and testing a particular situation; and    (ii) testing as wide range of situations as possible.
For example, (i) is a request to prioritize coverage of a situation in which a design-error may be present, such as when an interruption or an exception handling occurs. (ii) is a request to discover ideas that are not ordinarily conceived.
An extremely large number of patterns are required to be created or automatically generated to meet the request (ii). A large number of patterns cannot be created manually. Therefore, ordinarily, patterns that can be created manually are limited to patterns for the request (i).
The large number of patterns can be automatically generated using a pattern generator. However, to meet the request (ii), not only is the number of required patterns large, but it is also important that distribution of the patterns cover a range provided in a specification. To create a pattern generator such as the above, specification information is required to be understood in detail and reflected in a configuration of the pattern generator.
However, many procedures are required to create the pattern generator, and many errors occur. In addition, many return procedures are required when there are changes in the specification or misinterpretations of the specification. Therefore, the request “(ii) testing as wide a range of situations as possible” cannot be met.
At the same time, when a conventional technology, such as that in “Constraint Synthesis for Environment Modeling in Functional Verification”, is used, the pattern generator meeting the request (ii) can be automatically generated from a specification description (input restriction) without error. Furthermore, the changes in the specification and misinterpretations of the specification can be easily handled.
However, the conventional technology, such as that in “Constraint Synthesis for Environment Modeling in Functional Verification”, does not include a set-up that takes into consideration the request (i). A sequence in which the patterns are generated is decided by a random number not intended by a user. Therefore, all input patterns cannot be tested by logic simulation in the current hardware design verification because the number of required patterns is too large.
In the current hardware design verification, control of the sequence in which the patterns are generated or control of the distribution of the generated patterns is important. The conventional technology, such as that in “Constraint Synthesis for Environment Modeling in Functional Verification”, cannot control the sequence in which the patterns are generated or the distribution of the generated patterns. Therefore, the request “(i) targeting and testing a particular situation” cannot be met.